(*
 * Copyright (c) 2009, Palle Raabjerg
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   * Redistributions of source code must retain the above copyright notice,
 *     this list of conditions and the following disclaimer.
 *   * Redistributions in binary form must reproduce the above copyright notice,
 *     this list of conditions and the following disclaimer in the documentation
 *     and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 *)

open Alfp;;

type con_element = Clause of cl
		   | Comment of string;;
type commented_conjunction = (con_element list)

(* Shorthand functions. Using these can make axioms and encodings more readable in the code. *)
exception ClauseBuildError of string;;

(* Build a conjunction of clauses from a list *)
let rec cland_of_list flist =
  match flist with
    | (hd::[]) -> hd
    | (hd::tl) -> ClAnd(hd, cland_of_list tl)
    | [] -> raise (ClauseBuildError ("Bug: Please do not feed cland_of_list with an empty list. Be nice and give it something to work with."))

(* Build a conjunction of preconditions from a list *)
let rec preand_of_list flist =
  match flist with
    | (hd::[]) -> hd
    | (hd::tl) -> PreAnd(hd, preand_of_list tl)
    | [] -> raise (ClauseBuildError ("Bug: Please do not feed preand_of_list with an empty list. Be nice and give it something to work with."))

(* Prefix a clause with a number of universal quantifiers *)
let rec aquantify qlist clause =
  match qlist with
    | [] -> clause
    | (hd::tl) -> Forall(hd, aquantify tl clause)

(* Build a list of variables from a list of strings *)
let rec varlist strlist =
  List.fold_right (fun str variables ->
		     Var(str)::variables
		  ) strlist []

(* Build a list of constants from a list of strings *)
let rec constlist strlist =
  List.fold_right (fun str constants ->
		     Const(str)::constants
		  ) strlist []

(* - Relations - *)

(* Messages *)
let tpairrel = "TermPair"
let encrel = "Enc"
let namerel = "Name"
let tokrel = "OkTerm"

(* Types *)
let keyrel = "Key"
let pairrel = "Pair"
let chrel = "Ch"
let unrel = "Un"
let okrel = "Ok"

let typrel = "Type"

let maypf = "Q"

(* Effects *)
let effectrel = "Effect"

(* Generativity *)
let genrel = "Gen"
let nongenrel = "NonGen"

(* Equality *)
let eqrel = "eq"
let neqrel = "neq"

(* Type equality *)
let teqrel = "Teq"

(* Substitution for equality for dependent types. *)
let subsrel = "Subs"

let absrel = "Abs"
let apprel = "App"

let applyrel = "Apply"

(* Free names *)
let fnrel = "Fn"

(* Name in domain *)
let domrel = "Dom"

(* Elements of environments *)
let envrel = "Env"

(* Effects and non-effects *)
let effrel = "Eff"
let noneffrel = "NonEff"

(* Simple and non-simple environments *)
let simplerel = "Simple"
let nonsimplerel = "NonSimple"

(* Dependency *)
let deprel = "Dep"
let deprefrel = "DepRef"
let envdeprel = "EnvDep"

(* Initial and non-initial effects *)
let initrel = "Initial"
let noninitrel = "NotInitial"

(* Failure - Unary. Give it a string explaining failure. *)
let failrel = "Fail"

(* Admissibility *)
let admitsrel = "Admits"
let effadmitsrel = "EffAdmits"

(* Ranking of each relation *)
let ranklist = [(domrel, 1);     (* Domain relation *)
		(eqrel, 1);      (* Equality, rank 1 *)
		(neqrel, 2);     (* Inequality, rank 2 *)
		(tpairrel, 2);   (* Term relations, rank 2 *)
		(encrel, 2);
		(namerel, 2);
		(tokrel, 2);
		(subsrel, 2);    (* Subs relation, rank 2 *)
		(unrel, 2);      (* Un relation, rank 2 *)
		(keyrel, 3);     (* Other type relations, rank 3 *)
		(keyrel ^ maypf, 3);
		(pairrel, 3);
		(pairrel ^ maypf, 3);
		(chrel, 3);
		(chrel ^ maypf, 3);
		(okrel, 3);
		(okrel ^ maypf, 3);
		(absrel, 3);
		(absrel ^ maypf, 3);
		(apprel, 3);
		(apprel ^ maypf, 3);
		(applyrel, 3);
		(typrel, 3);     (* Type relation *)
		(teqrel, 3);     (* Type equality, rank 3 *)
		(genrel, 3);     (* Generativity and non-generativity, rank 3 *)
		(nongenrel, 3);
		(envdeprel, 3);  (* Dependency of effect variables on environments and each other, rank 3 and 4 *)
		(deprel, 4);
		(deprefrel, 4);
		(envrel, 4);     (* Environment relation, rank 4 *)
		(simplerel, 4);  (* Simplicity relations, rank 4 *)
		(nonsimplerel, 4);
		(effectrel, 4);  (* Effect relations, rank 4 *)
		(effrel, 4);
		(noneffrel, 4);
		(initrel, 4);    (* Initial and noninitial effects, rank 4 *)
		(noninitrel, 4);
		(fnrel, 5);
		(admitsrel, 6);  (* Admissibility, rank 6 *)
		(effadmitsrel, 6);
		(failrel, 6)
	       ]

(* - Axioms - *)

(* Equality and inequality *)
let eqneq = ClAnd(Forall("x",
			 CPredicate(eqrel, [Var("x"); Var("x")])),
		  Forall("x", Forall("y",
				     Leadsto(NegPredicate(eqrel, [Var("x"); Var("y")]),
					     CPredicate(neqrel, [Var("x"); Var("y")])))));;

let axioms_eqneq = [Comment("Equality and inequality on names. We simply describe that every distinct " ^
			      "name is equal to itself, and not equal to any other name.");
		    Clause(eqneq)]

(* Generativity *)
let ax_un = Forall("t",
		    Leadsto(PPredicate(unrel, [Var("t")]),
			    CPredicate(genrel, [Var("t")])))
let ax_key = Forall("t1", Forall("t2",
				 Leadsto(PPredicate(keyrel, [Var("t1"); Var("t2")]),
					 CPredicate(genrel, [Var("t1")]))))
let ax_ch = Forall("t1", Forall("t2",
				Leadsto(PPredicate(chrel, [Var("t1"); Var("t2")]),
					CPredicate(genrel, [Var("t1")]))))
let ax_pair = Forall("t1", Forall("x", Forall("t2", Forall("t3",
							   Leadsto(PPredicate(pairrel, [Var("t1"); Var("x"); Var("t2"); Var("t3")]),
								   CPredicate(nongenrel, [Var("t1")]))))))
let ax_ok = Forall("t", Forall("r",
			       Leadsto(PPredicate(okrel, [Var("t"); Var("r")]),
				       CPredicate(nongenrel, [Var("t")]))))

let axioms_gen = [Comment("Generativity and non-generativity." ^
			    "These formulae map types to the generativity relations.");
		  Clause(ax_un);
		  Clause(ax_key);
		  Clause(ax_ch);
		  Clause(ax_pair);
		  Clause(ax_ok)
		 ]

(* Type equality *)
(* Note: Doing this kind of type equality for the Un type would be pointless,
 * as Un does not contain any type or effect. *)
let pair_pre = PreAnd(PPredicate(pairrel, [Var("t1'"); Var("x1"); Var("t2"); Var("t3")]),
		      PreAnd(PPredicate(pairrel, [Var("t1''"); Var("x2"); Var("t4"); Var("t5")]),
			     PPredicate(teqrel, [Var("t1'"); Var("t1''")])))
let pair_cl = ClAnd(CPredicate(teqrel, [Var("t2"); Var("t4")]), CPredicate(teqrel, [Var("t3"); Var("t5")]))
let ax_teq_pair = aquantify ["x1"; "x2"; "t1'"; "t1''"; "t2"; "t3"; "t4"; "t5"]
  (Leadsto(pair_pre,
	   pair_cl)
  )

let key_pre = PreAnd(PPredicate(keyrel, [Var("t1'"); Var("t2")]),
		     PreAnd(PPredicate(keyrel, [Var("t1''"); Var("t3")]),
			    PPredicate(teqrel, [Var("t1'"); Var("t1''")])))
let ax_teq_key = aquantify ["t1'"; "t1''"; "t2"; "t3"]
  (Leadsto(key_pre,
	   CPredicate(teqrel, [Var("t2"); Var("t3")]))
  )

let ch_pre = PreAnd(PPredicate(chrel, [Var("t1'"); Var("t2")]),
		    PreAnd(PPredicate(chrel, [Var("t1''"); Var("t3")]),
			   PPredicate(teqrel, [Var("t1'"); Var("t1''")])))
let ax_teq_ch = aquantify ["t1'"; "t1''"; "t2"; "t3"]
  (Leadsto(ch_pre,
	   CPredicate(teqrel, [Var("t2"); Var("t3")]))
  )

let ok_pre = PreAnd(PPredicate(okrel, [Var("t1'"); Var("s1")]),
		    PreAnd(PPredicate(okrel, [Var("t1''"); Var("s2")]),
			   PPredicate(teqrel, [Var("t1'"); Var("t1''")])))
let ax_teq_ok = aquantify ["t1'"; "t1''"; "s1"; "s2"]
  (Leadsto(ok_pre,
	   CPredicate(teqrel, [Var("s1"); Var("s2")]))
  )

let axioms_teq = [Comment("Type equality. We say that if two types are equal, then their inner types are also equal.");
		  Clause(ax_teq_pair);
		  Clause(ax_teq_key);
		  Clause(ax_teq_ch);
		  Clause(ax_teq_ok)
		 ]

(* General type equality axioms *)
let ax_teq_reflex1 = Forall("t", CPredicate(teqrel, [Var("t"); Var("t")]))
let ax_teq_reflex2 = aquantify ["t1"; "t2"]
  (Leadsto(PPredicate(teqrel, [Var("t1"); Var("t2")]),
	   CPredicate(teqrel, [Var("t2"); Var("t1")])))

let ax_teq_trans = aquantify ["t1"; "t2"; "t3"]
  (Leadsto(PreAnd(PPredicate(teqrel, [Var("t1"); Var("t2")]),
		  PPredicate(teqrel, [Var("t2"); Var("t3")])),
	   CPredicate(teqrel, [Var("t1"); Var("t3")])))

let axioms_genteq = [Comment("Type equality is both reflexive and transitive.");
		     Clause(ax_teq_reflex1);
		     Clause(ax_teq_reflex2);
		     Clause(ax_teq_trans)
		    ]

(* Dependent types *)

(* Substitution on terms *)
let ax_tok_subs = aquantify ["n"; "m'"; "m"]
  (Leadsto(PPredicate(tokrel, [Var("n")]),
	   CPredicate(subsrel, varlist ["n"; "n"; "m'"; "m"])))

let ax_name_subs = aquantify ["m'"; "m"]
  (Leadsto(PPredicate(namerel, [Var("m")]),
	   CPredicate(subsrel, varlist ["m'"; "m"; "m'"; "m"])))

let ax_tpair_subs = aquantify ["n"; "n1'"; "n1"; "m'"; "m"; "n2'"; "n2"; "n'"]
  (Leadsto(preand_of_list [PPredicate(subsrel, varlist ["n1'"; "n1"; "m'"; "m"]);
			   PPredicate(subsrel, varlist ["n2'"; "n2"; "m'"; "m"]);
			   PPredicate(tpairrel, varlist ["n";  "n1";  "n2"]);
			   PPredicate(tpairrel, varlist ["n'"; "n1'"; "n2'"])],
	   CPredicate(subsrel, varlist ["n'"; "n"; "m'"; "m"])
	  )
  )

let ax_enc_subs = aquantify ["n"; "n1'"; "n1"; "m'"; "m"; "n2'"; "n2"; "n'"]
  (cland_of_list [
     Leadsto(preand_of_list [PPredicate(subsrel, varlist ["n1'"; "n1"; "m'"; "m"]);
			     PPredicate(subsrel, varlist ["n2'"; "n2"; "m'"; "m"]);
			     PPredicate(encrel, varlist ["n";  "n1";  "n2"]);
			     PPredicate(encrel, varlist ["n'"; "n1'"; "n2'"])],
	     CPredicate(subsrel, varlist ["n'"; "n"; "m'"; "m"])
	    )
   ])

let axioms_subs = [Comment("Substitution on terms");
		   Clause(ax_tok_subs);
		   Clause(ax_name_subs);
		   Clause(ax_tpair_subs);
		   Clause(ax_enc_subs)
		  ]

(* Substitution on effects *)

let ax_effect_subs = aquantify ["n"; "n'"; "l"; "m"; "m'"; "s"; "s'"]
  (Leadsto(PreAnd(PPredicate (effectrel, varlist ["l"; "n"; "s'"]),
		  PPredicate (subsrel, varlist ["n'"; "n"; "m'"; "m"])
		 ),
	   CPredicate(effectrel, varlist ["l"; "n'"; "s"])
	  )
  )

let axioms_effsubs = [Comment("Substitution on effects");
		      Clause(ax_effect_subs)
		     ]

(* Substitution on types *)
(*let ax_ok_subs = aquantify ["t"; "t'"; "s"; "s'"; "m"; "m'"]
  (Leadsto(preand_of_list [PPredicate(okrel, varlist ["t"; "s"]);
			   PPredicate(subsrel, varlist ["s'"; "s"; "m'"; "m"]);
			   PPredicate(okrel, varlist ["t'"; "s'"])
			  ],
	   CPredicate(subsrel, varlist ["t'"; "t"; "m'"; "m"])
	  )
  )

let ax_ch_subs = aquantify ["t"; "t'"; "t1"; "t1'"; "m"; "m'"]
  (Leadsto(preand_of_list [PPredicate(chrel, varlist ["t"; "t1"]);
			   PPredicate(subsrel, varlist ["t1'"; "t1"; "m'"; "m"]);
			   PPredicate(chrel, varlist ["t'"; "t1'"])
			  ],
	   CPredicate(subsrel, varlist ["t'"; "t"; "m'"; "m"])
	  )
  )

let ax_key_subs = aquantify ["t"; "t'"; "t1"; "t1'"; "m"; "m'"]
  (Leadsto(preand_of_list [PPredicate(keyrel, varlist ["t"; "t1"]);
			   PPredicate(subsrel, varlist ["t1'"; "t1"; "m'"; "m"]);
			   PPredicate(keyrel, varlist ["t'"; "t1'"])
			  ],
	   CPredicate(subsrel, varlist ["t'"; "t"; "m'"; "m"])
	  )
  )

let ax_pair_subs = aquantify ["t"; "t1"; "t2"; "t'"; "t1'"; "t2'"; "m"; "m'"; "x"]
  (Leadsto(preand_of_list [PPredicate(pairrel, varlist ["t"; "x"; "t1"; "t2"]);
			   PPredicate(subsrel, varlist ["t1'"; "t1"; "m'"; "m"]);
			   PPredicate(subsrel, varlist ["t2'"; "t2"; "m'"; "m"]);
			   PPredicate(pairrel, varlist ["t'"; "x"; "t1'"; "t2'"])
			  ],
	   CPredicate(subsrel, varlist ["t'"; "t"; "m'"; "m"])
	  )
  )

let ax_un_subs = aquantify ["t"; "t'"; "m'"; "m"]
  (Leadsto(PreAnd(PPredicate(unrel, [Var("t")]),
		  PPredicate(unrel, [Var("t'")])
		 ),
	   CPredicate(subsrel, varlist ["t'"; "t"; "m'"; "m"])
	  )
  )

let axioms_typsubs = [Comment("Substitution on types");
		      Clause(ax_ok_subs);
		      Clause(ax_ch_subs);
		      Clause(ax_key_subs);
		      Clause(ax_pair_subs);
		      Clause(ax_un_subs)
		     ]*)

(* Abstraction on types *)
(* Woah. The definitions of abstraction and application are a bit confused.
 * Hey! Subject for next supervisor meeting. *)
(*let ax_abs_subs = aquantify ["n"; "n'"; "m"; "m'"; "t"; "t'"]
  (Leadsto(preand_of_list [PPredicate(typrel, varlist ["n"; "t"]);
			   PPredicate(subsrel, varlist ["t'"; "t"; "m'"; "m"]);
			   PPredicate(typrel, varlist ["n'"; "t"])
			  ],
	   CPredicate(absrel, varlist ["n'"; "t"; "m'"; "m"])
	  )
  )

let axioms = List.append axioms [Comment("Abstraction on types");
				 Clause(ax_abs_subs)
				]*)

(* Application on types *)
(*let ax_app_subs = aquantify ["v"; "v'"; "n"; "m"; "m1"; "m2"; "m3"]
  (
  )*)

(* Free names of terms *)
let ax_name_fn = Forall("n",
			Leadsto(PPredicate(namerel, [Var("n")]),
				CPredicate(fnrel, varlist ["n"; "n"])))

let ax_tpair_fn = aquantify ["n"; "n1"; "n2"; "m"]
  (Leadsto(PreAnd(Or(PPredicate(fnrel, varlist ["m"; "n1"]),
		     PPredicate(fnrel, varlist ["m"; "n2"])),
		  PPredicate(tpairrel, varlist ["n"; "n1"; "n2"])),
	   CPredicate(fnrel, varlist ["m"; "n"]))
  )

let ax_enc_fn = aquantify ["n"; "n1"; "n2"; "m"]
  (Leadsto(PreAnd(Or(PPredicate(fnrel, varlist ["m"; "n1"]),
		     PPredicate(fnrel, varlist ["m"; "n2"])),
		  PPredicate(encrel, varlist ["n"; "n1"; "n2"])),
	   CPredicate(fnrel, varlist ["m"; "n"]))
  )

let axioms_fn = [Comment("Free names of terms. A name is always free in itself. For pairs and encryptions, if a name is free in either element, it is free for the pair, or encryption.");
		 Clause(ax_name_fn);
		 Clause(ax_tpair_fn);
		 Clause(ax_enc_fn);
		]

(* Free names of types *)

let ax_ch_fn = aquantify ["t"; "t1"; "m"]
  (Leadsto(PreAnd(PPredicate(chrel, varlist ["t"; "t1"]),
		  PPredicate(fnrel, varlist ["m"; "t1"])
		 ),
	   CPredicate(fnrel, varlist ["m"; "t"])
	  )
  )

let ax_key_fn = aquantify ["t"; "t1"; "m"]
  (Leadsto(PreAnd(PPredicate(keyrel, varlist ["t"; "t1"]),
		  PPredicate(fnrel, varlist ["m"; "t1"])
		 ),
	   CPredicate(fnrel, varlist ["m"; "t"])
	  )
  )

let ax_pair_fn = aquantify ["t"; "t1"; "t2"; "x"; "m"]
  (Leadsto(preand_of_list [PPredicate(pairrel, varlist ["t"; "x"; "t1"; "t2"]);
			   Or(PPredicate(fnrel, varlist ["m"; "t1"]),
			      PPredicate(fnrel, varlist ["m"; "t2"]));
			   PPredicate(neqrel, varlist ["m"; "x"])
			  ],
	   CPredicate(fnrel, varlist ["m"; "t"])
	  )
  )

let ax_ok_fn = aquantify ["t"; "s"; "m"]
  (Leadsto(PreAnd(PPredicate(okrel, varlist ["t"; "s"]),
		  PPredicate(fnrel, varlist ["m"; "s"])
		 ),
	   CPredicate(fnrel, varlist ["m"; "t"])
	  )
  )

let ax_effects_fn = aquantify ["m"; "n"; "l"; "s"]
  (Leadsto(PreAnd(PPredicate(fnrel, varlist ["n"; "m"]),
		  PPredicate(effectrel, varlist ["l"; "m"; "s"])
		 ),
	   CPredicate(fnrel, varlist ["n"; "s"])
	  )
  )

let axioms_typfn = [Comment("Free names of types");
		    Clause(ax_ch_fn);
		    Clause(ax_key_fn);
		    Clause(ax_pair_fn);
		    Clause(ax_ok_fn);
		    Clause(ax_effects_fn);
		   ]

let ax_may_key = aquantify ["t"; "t1"]
  (Leadsto(PreAnd(PPredicate(keyrel ^ maypf, varlist ["t"; "t1"]),
		  NegPredicate(unrel, [Var("t")])),
	   CPredicate(keyrel, varlist ["t"; "t1"])))

let ax_may_pair = aquantify ["t"; "x"; "t1"; "t2"]
  (Leadsto(PreAnd(PPredicate(pairrel ^ maypf, varlist ["t"; "x"; "t1"; "t2"]),
		  NegPredicate(unrel, [Var("t")])),
	   CPredicate(pairrel, varlist ["t"; "x"; "t1"; "t2"])))

let ax_may_ch = aquantify ["t"; "t1"]
  (Leadsto(PreAnd(PPredicate(chrel ^ maypf, varlist ["t"; "t1"]),
		  NegPredicate(unrel, [Var("t")])),
	   CPredicate(chrel, varlist ["t"; "t1"])))

let ax_may_ok = aquantify ["t"; "s"]
  (Leadsto(PreAnd(PPredicate(okrel ^ maypf, varlist ["t"; "s"]),
		  NegPredicate(unrel, [Var("t")])),
	   CPredicate(okrel, varlist ["t"; "s"])))

let ax_may_abs = aquantify ["v"; "u"; "m"; "t"]
  (Leadsto(PreAnd(PPredicate(absrel ^ maypf, varlist ["v"; "u"; "m"; "t"]),
		  NegPredicate(unrel, [Var("v")])),
	   CPredicate(absrel, varlist ["v"; "u"; "m"; "t"])))

let ax_may_app = aquantify ["v"; "u"; "n"]
  (Leadsto(PreAnd(PPredicate(apprel ^ maypf, varlist ["v"; "u"; "n"]),
		  NegPredicate(unrel, [Var("v")])),
	   CPredicate(apprel, varlist ["v"; "u"; "n"])))

let axioms_may = [Comment("Possible types. These axioms were added to the ones of \\cite{HHWIP}, " ^
			    "to describe how the $=$ and $\\mayeq$ type relations interact. " ^
			    "The $\\Rel{" ^ unrel ^ "}$ relation is populated by the generation rules in a stratum prior to all " ^
			    "the other type relations. In that stratum, all the types that must be \\Un{} are found, and a stratum " ^
			    "later, the other type relations are populated from the $\\mayeq$ relations to fill in those types that " ^
			    "are not \\Un{}.");
		  Clause(ax_may_key);
		  Clause(ax_may_pair);
		  Clause(ax_may_ch);
		  Clause(ax_may_ok);
		  Clause(ax_may_abs);
		  Clause(ax_may_app)
		 ]

(* Effect and Non-effect axioms *)
let ax_eff_ok = aquantify ["t"; "s"]
  (Leadsto(PPredicate(okrel, varlist ["t"; "s"]),
	   CPredicate(effrel, [Var("t")])))

let ax_eff_pair = aquantify ["x"; "t"; "t1"; "t2"]
  (Leadsto(PPredicate(pairrel, varlist ["t"; "x"; "t1"; "t2"]),
	   CPredicate(noneffrel, [Var("t")])))

let ax_eff_key = aquantify ["t"; "t1"]
  (Leadsto(PPredicate(keyrel, varlist ["t"; "t1"]),
	   CPredicate(noneffrel, [Var("t")])))

let ax_eff_ch = aquantify ["t"; "t1"]
  (Leadsto(PPredicate(chrel, varlist ["t"; "t1"]),
	   CPredicate(noneffrel, [Var("t")])))

let ax_eff_un =
  Forall("t",
	 Leadsto(PPredicate(unrel, [Var("t")]),
		 CPredicate(noneffrel, [Var("t")]))
	)

let ax_eff_teq = aquantify ["t1"; "t2"]
  (Leadsto(PreAnd(PPredicate(effrel, [Var("t1")]),
		  PPredicate(teqrel, varlist ["t1"; "t2"])),
	   CPredicate(effrel, [Var("t2")])))

let ax_noneff_teq = aquantify ["t1"; "t2"]
  (Leadsto(PreAnd(PPredicate(noneffrel, [Var("t1")]),
		  PPredicate(teqrel, varlist ["t1"; "t2"])),
	   CPredicate(noneffrel, [Var("t2")])))

let axioms_eff = [Comment("Axioms for deciding which types contain effects, and which do not.");
		  Clause(ax_eff_ok);
		  Clause(ax_eff_pair);
		  Clause(ax_eff_key);
		  Clause(ax_eff_ch);
		  Clause(ax_eff_un);
		  Clause(ax_eff_teq);
		  Clause(ax_noneff_teq);
		 ]

(* Simple and nonsimple environments *)
let ax_simple = aquantify ["e"; "t"; "x"]
  (Leadsto(PreAnd(PPredicate(envrel, varlist ["x"; "t"; "e"]),
		  PPredicate(effrel, [Var("t")])),
	   CPredicate(simplerel, [Var("e")])))

let ax_nonsimple =
  Forall("e",
	 Leadsto(Exists("t", Exists("x",
				    PreAnd(PPredicate(envrel, varlist ["x"; "t"; "e"]),
					   PPredicate(noneffrel, [Var("t")])))),
		 CPredicate(nonsimplerel, [Var("e")])))

let axioms_simplicity = [Comment("We decide which environments are simple and which are non-simple.");
			 Clause(ax_simple);
			 Clause(ax_nonsimple)
			]

let ax_dep = aquantify ["e"; "x"; "t"; "s"; "s'"]
  (Leadsto(preand_of_list [PPredicate(envrel, varlist ["x"; "t"; "e"]);
			   PPredicate(okrel, varlist ["t"; "s'"]);
			   PPredicate(envdeprel, varlist ["s"; "e"])],
	   CPredicate(deprel, varlist ["s"; "s'"])))

let ax_dep_trans = aquantify ["s1"; "s2"; "s3"]
  (Leadsto(preand_of_list [PPredicate(deprel, varlist ["s1"; "s2"]);
			   PPredicate(deprel, varlist ["s2"; "s3"]);],
	   CPredicate(deprel, varlist ["s1"; "s3"])))

let axioms_dependency = [Comment("We find dependencies between effect variables.");
			 Clause(ax_dep);
			 Clause(ax_dep_trans)
			]

let ax_initial = aquantify ["s"; "e"]
  (Leadsto(PreAnd(PPredicate(simplerel, [Var("e")]),
		  PPredicate(envdeprel, varlist ["s"; "e"])),
	   CPredicate(initrel, [Var("s")])))

let ax_noninitial = aquantify ["s"; "e"]
  (Leadsto(PreAnd(PPredicate(envdeprel, varlist ["s"; "e"]),
		  PPredicate(nonsimplerel, [Var("e")])),
	   CPredicate(noninitrel, [Var("s")])
	  ))

let axioms_initiality = [Comment("We find initial and non-initial effect variables.");
			 Clause(ax_initial);
			 Clause(ax_noninitial)
			]

let ax_admits = aquantify ["m"; "e"; "n"]
  (Leadsto(Or(NegPredicate(fnrel, varlist ["n"; "m"]),
	      PPredicate(domrel, varlist ["n"; "e"])),
	   CPredicate(admitsrel, varlist ["e"; "m"])))

let ax_effadmits = aquantify ["m"; "e"; "s"]
  (Leadsto(PreAnd(PPredicate(admitsrel, varlist ["e"; "m"]),
		  PPredicate(envdeprel, varlist ["s"; "e"])),
	   CPredicate(effadmitsrel, varlist ["s"; "m"])))

let axioms_admissibility = [Comment("We find which messages are admitted by environments and effects");
			    Clause(ax_admits);
			    Clause(ax_effadmits)
			   ]

let ax_abs_ch = aquantify ["t1"; "t1'"; "t2"; "m"; "x"]
  (Leadsto(PreAnd(PPredicate(chrel, varlist ["t1"; "t2"]),
		  PPredicate(absrel, varlist ["t1'"; "t1"; "m"; "x"])),
	   CPredicate(absrel, varlist ["t1'"; "t2"; "m"; "x"])))

let ax_abs_key = aquantify ["t1"; "t1'"; "t2"; "m"; "x"]
  (Leadsto(PreAnd(PPredicate(keyrel, varlist ["t1"; "t2"]),
		  PPredicate(absrel, varlist ["t1'"; "t1"; "m"; "x"])),
	   CPredicate(absrel, varlist ["t1'"; "t2"; "m"; "x"])))

let ax_abs_pair = aquantify ["t1"; "t1'"; "t2"; "t3"; "t2'"; "m"; "x1"; "x2"]
  (Leadsto(PreAnd(PPredicate(pairrel, varlist ["t1"; "x1"; "t2"; "t3"]),
		  PPredicate(absrel, varlist ["t1'"; "t1"; "m"; "x2"])),
	   ClAnd (CPredicate(absrel, varlist ["t1'"; "t2"; "m"; "x2"]),
		  CPredicate(absrel, varlist ["t1'"; "t3"; "m"; "x2"]))))

let ax_abs_ok = aquantify ["t1"; "t1'"; "s"; "m"; "x"]
  (Leadsto(PreAnd(PPredicate(okrel, varlist ["t1"; "s"]),
		  PPredicate(absrel, varlist ["t1'"; "t1"; "m"; "x"])),
	   CPredicate(absrel, varlist ["t1'"; "s"; "m"; "x"])))

let axioms_abstraction = [Comment("Axioms for abstraction. Propagates abstraction into abstracted type.");
			  Clause(ax_abs_ch);
			  Clause(ax_abs_key);
			  Clause(ax_abs_pair);
			  Clause(ax_abs_ok)
			 ]

let ax_app_ch = aquantify ["t1"; "t2"; "t3"; "t4"; "m1"; "m2"; "x"]
  (Leadsto(preand_of_list [PPredicate(chrel, varlist ["t1"; "t2"]);
			   PPredicate(absrel, varlist ["t1"; "t3"; "m1"; "x"]);
			   PPredicate(apprel, varlist ["t4"; "t1"; "m2"])
			  ],
	   ClAnd(CPredicate(chrel, varlist["t4"; "t2"]),
		 CPredicate(applyrel, varlist["t4"; "t4"; "m2"; "m1"]))))

let ax_app_key = aquantify ["t1"; "t2"; "t3"; "t4"; "m1"; "m2"; "x"]
  (Leadsto(preand_of_list [PPredicate(keyrel, varlist ["t1"; "t2"]);
			   PPredicate(absrel, varlist ["t1"; "t3"; "m1"; "x"]);
			   PPredicate(apprel, varlist ["t4"; "t1"; "m2"])
			  ],
	   ClAnd(CPredicate(keyrel, varlist["t4"; "t2"]),
		 CPredicate(applyrel, varlist["t4"; "t4"; "m2"; "m1"]))))

let ax_app_pair = aquantify ["t1"; "t2"; "t3"; "t4"; "t5"; "m1"; "m2"; "x"; "x1"]
  (Leadsto(preand_of_list [PPredicate(pairrel, varlist ["t1"; "x1"; "t2"; "t5"]);
			   PPredicate(absrel, varlist ["t1"; "t3"; "m1"; "x"]);
			   PPredicate(apprel, varlist ["t4"; "t1"; "m2"])
			  ],
	   ClAnd(CPredicate(pairrel, varlist["t4"; "x1"; "t2"; "t5"]),
		 CPredicate(applyrel, varlist["t4"; "t4"; "m2"; "m1"]))))

let ax_app_ok = aquantify ["t1"; "s"; "t3"; "t4"; "m1"; "m2"; "x"]
  (Leadsto(preand_of_list [PPredicate(okrel, varlist ["t1"; "s"]);
			   PPredicate(absrel, varlist ["t1"; "t3"; "m1"; "x"]);
			   PPredicate(apprel, varlist ["t4"; "t1"; "m2"])
			  ],
	   ClAnd(CPredicate(okrel, varlist["t4"; "s"]),
		 CPredicate(applyrel, varlist["t4"; "t4"; "m2"; "m1"]))))

let axioms_application = [Comment("Axioms for application. Indicates application of a type abstraction.");
			  Clause(ax_app_ch);
			  Clause(ax_app_key);
			  Clause(ax_app_pair);
			  Clause(ax_app_ok)
			 ]

let ax_apply_ch = aquantify ["t"; "t1"; "t2"; "m1"; "m2"]
  (Leadsto(PreAnd(PPredicate(chrel, varlist ["t1"; "t2"]),
		  PPredicate(applyrel, varlist ["t"; "t1"; "m2"; "m1"])),
	   CPredicate(applyrel, varlist ["t"; "t2"; "m2"; "m1"])))

let ax_apply_key = aquantify ["t"; "t1"; "t2"; "m1"; "m2"]
  (Leadsto(PreAnd(PPredicate(keyrel, varlist ["t1"; "t2"]),
		  PPredicate(applyrel, varlist ["t"; "t1"; "m2"; "m1"])),
	   CPredicate(applyrel, varlist ["t"; "t2"; "m2"; "m1"])))

let ax_apply_pair = aquantify ["t"; "t1"; "t2"; "t3"; "m1"; "m2"; "x"]
  (Leadsto(PreAnd(PPredicate(pairrel, varlist ["t1"; "x"; "t2"; "t3"]),
		  PPredicate(applyrel, varlist ["t"; "t1"; "m2"; "m1"])),
	   ClAnd(CPredicate(applyrel, varlist ["t"; "t2"; "m2"; "m1"]),
		 CPredicate(applyrel, varlist ["t"; "t3"; "m2"; "m1"]))))

let ax_apply_ok = aquantify ["t"; "t1"; "s"; "m1"; "m2"]
  (Leadsto(PreAnd(PPredicate(okrel, varlist ["t1"; "s"]),
		  PPredicate(applyrel, varlist ["t"; "t1"; "m2"; "m1"])),
	   CPredicate(applyrel, varlist ["t"; "s"; "m2"; "m1"])))

let axioms_apply = [Comment("Axioms for apply propagation. Propagates an application to inner types.");
		    Clause(ax_apply_ch);
		    Clause(ax_apply_key);
		    Clause(ax_apply_pair);
		    Clause(ax_apply_ok)
		   ]

(* Unification of isolated variables *)
let ax_uni_ch = aquantify ["t1"; "t1'"; "t2"]
  (Leadsto(PreAnd(PPredicate(chrel, varlist ["t1"; "t2"]),
		  PPredicate(teqrel, varlist ["t1"; "t1'"])),
	   CPredicate(chrel, varlist ["t1'"; "t2"])))

let ax_uni_key = aquantify ["t1"; "t1'"; "t2"]
  (Leadsto(PreAnd(PPredicate(keyrel, varlist ["t1"; "t2"]),
		  PPredicate(teqrel, varlist ["t1"; "t1'"])),
	   CPredicate(keyrel, varlist ["t1'"; "t2"])))

let ax_uni_pair = aquantify ["t1"; "t1'"; "t2"; "t3"; "x"]
  (Leadsto(PreAnd(PPredicate(pairrel, varlist ["t1"; "x"; "t2"; "t3"]),
		  PPredicate(teqrel, varlist ["t1"; "t1'"])),
	   CPredicate(pairrel, varlist ["t1'"; "x"; "t2"; "t3"])))

let ax_uni_ok = aquantify ["t1"; "t1'"; "t2"]
  (Leadsto(PreAnd(PPredicate(okrel, varlist ["t1"; "t2"]),
		  PPredicate(teqrel, varlist ["t1"; "t1'"])),
	   CPredicate(okrel, varlist ["t1'"; "t2"])))

let ax_uni_app = aquantify ["t1"; "t1'"; "t2"; "m"]
  (Leadsto(PreAnd(PPredicate(apprel, varlist ["t1"; "t2"; "m"]),
		  PPredicate(teqrel, varlist ["t1"; "t1'"])),
	   CPredicate(apprel, varlist ["t1'"; "t2"; "m"])))

let ax_uni_abs = aquantify ["t1"; "t1'"; "t2"; "m"; "x"]
  (Leadsto(PreAnd(PPredicate(absrel, varlist ["t1"; "t2"; "m"; "x"]),
		  PPredicate(teqrel, varlist ["t1"; "t1'"])),
	   CPredicate(absrel, varlist ["t1'"; "t2"; "m"; "x"])))

let axioms_unification = [Comment("Unification axioms. This is also a way of assigning types to isolated type variables.");
			  Clause(ax_uni_ch);
			  Clause(ax_uni_key);
			  Clause(ax_uni_pair);
			  Clause(ax_uni_ok);
			  Clause(ax_uni_app);
			  Clause(ax_uni_abs)
			 ]

(* Proposition 1 *)
let ax_initial_effects = aquantify ["s"; "s1"; "e"; "m"]
  (Leadsto(preand_of_list [PPredicate(effadmitsrel, varlist ["s1"; "m"]);
			   PPredicate(deprefrel, varlist ["s"; "s1"]);
			   PPredicate(initrel, [Var("s")]);
			   PPredicate(envrel, varlist ["l"; "m"; "e"])
			  ],
	   CPredicate(effectrel, varlist ["l"; "m"; "s1"])))

(* Proposition 4 *)
(*let ax_noninitial_effects = *)

(* Proposition 5 *)
(*let ax_semiinitial_effects =*)

let axioms = List.concat [axioms_eqneq;
			  axioms_gen;
			  axioms_teq;
			  axioms_genteq;
			  axioms_subs;
			  axioms_effsubs;
			  (*axioms_typsubs;*)
			  axioms_fn;
			  axioms_typfn;
			  axioms_may;
			  axioms_eff;
			  axioms_simplicity;
			  axioms_dependency;
			  axioms_initiality;
			  axioms_admissibility;
			  axioms_abstraction;
			  axioms_application;
			  axioms_apply;
			  axioms_unification
			 ]

(* Conjunction of axioms *)
let axiom_conjunction =
  let filtered_list = List.fold_right (fun element accum_list ->
					 match element with
					   | Comment(_) -> accum_list
					   | Clause(cl) -> cl::accum_list
				      ) axioms []
  in
  let ax_hd, ax_tl = (List.hd filtered_list, List.tl filtered_list) in
    List.fold_left (fun ax_accum cl ->
		      ClAnd(ax_accum, cl)
		   ) ax_hd ax_tl

(*let ax_*)
